es:ES, C, T:Type, S1, S2, Ack1, Ack2:(CCE), R1, Req1, R2, Req2:(CE),
codes1:(j,i:Ce:{x:E| S1(j,i,x)} state@loc(e)T),
codes2:(j,i:Ce:{x:E| S2(j,i,x)} state@loc(e)T),
decodes1:(i:Ce:{x:E| R1(i,x)} state@loc(e)T),
decodes2:(i:Ce:{x:E| R2(i,x)} state@loc(e)T), dec_R1:(i:Ce:EDec(R1(i,e))).
(i:C, e:E. (R1(i,e) & R2(i,e)))
 (dec_S1:(j,i:Ce:EDec(S1(j,i,e))).
 (j, j', i:C, e:E. (S1(j,i,e) & S2(j',i,e)))
  (i:C, e:E. Dec(j:C. (S1(j,i,e))))
  (i:C, e:E. Dec(j:C. (S2(j,i,e))))
  (i:C, e:E. Dec(R2(i,e)))
  for clients C sends FIFO
  forfrom j to i via (S1[j,i],codes1)
  forreceives at i via (R1[i],decodes1)  requests Req1[j] are acknowledged by Ack1[j,i]
  for clients C sends FIFO
  forfrom j to i via (S2[j,i],codes2)
  forreceives at i via (R2[i],decodes2)  requests Req2[j] are acknowledged by Ack2[j,i]
  switch between fifo+ send S1(j,i,e)
  switch between fifo+ srequest Req1(i,e)
  switch between fifo+ sacknowledge Ack1(j,i,e) and
  switch between fifo+ send S2(j,i,e) request Req2(i,e) acknowledge Ack2(j,i,e)
  for clients C sends FIFO
  forfrom j to i via (j,i,e. (S1(j,i,e))  (S2(j,i,e))[j,i],[S1? codes1 : codes2])
  forreceives at i via (i,e. (R1(i,e))  (R2(i,e))[i],[R1 ? decodes1 : decodes2])) 

latex

Definitions

t  ...$L, e c e', False, x. t(x), True, T, if p:P then A(p) else B fi , [S? codes1 : codes2], [R ? decodes1 : decodes2], P  Q, P  Q, A c B, {T}, P  Q, x,y. t(x;y), x,y,z. t(x;y;z), t  T, for clients C sends FIFO   from j to i via (S[j,i],codes)   receives at i via (R[i],decodes), x(s1,s2), x(s1,s2,s3), x:A. B(x), P & Q, A, P  Q, , x:A. B(x), fifo+switch, x(s), SqStable(P), Q f P, Q  f P, Dec(P), x  {FDLNOr12445}, fifo+

Lemmas

es-causle weakening, es-causl transitivity1, causal-order-preserving-interleaving, es-causl wf, es-causle transitivity, causal-order-preserving wf, decidable es-causle, sq stable from decidable, true wf, squash wf, es-state-when wf, antecedent-surjection functionality wrt iff, antecedent-surjection wf, es-causle wf, subtype rel function, event system wf, es-loc wf, es-state wf, not wf, decidable wf, fifo+ wf, fifo+switch wf, es-E wf, combine-antecedent-surjections